0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 85 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 40 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
rotateD_in_ga(.(T16, T17), T7) → U4_ga(T16, T17, T7, append2A_in_aag(X40, X41, T17))
append2A_in_aag(.(T32, X89), X90, .(T32, T33)) → U1_aag(T32, X89, X90, T33, append2A_in_aag(X89, X90, T33))
append2A_in_aag([], T38, T38) → append2A_out_aag([], T38, T38)
U1_aag(T32, X89, X90, T33, append2A_out_aag(X89, X90, T33)) → append2A_out_aag(.(T32, X89), X90, .(T32, T33))
U4_ga(T16, T17, T7, append2A_out_aag(X40, X41, T17)) → rotateD_out_ga(.(T16, T17), T7)
rotateD_in_ga(.(T16, T17), T7) → U5_ga(T16, T17, T7, append2A_in_aag(T20, T21, T17))
U5_ga(T16, T17, T7, append2A_out_aag(T20, T21, T17)) → U6_ga(T16, T17, T7, append1B_in_ggga(T21, T16, T20, T7))
append1B_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U2_ggga(T64, T65, T66, T67, T69, append1B_in_ggga(T65, T66, T67, T69))
append1B_in_ggga([], T79, T80, .(T79, T80)) → append1B_out_ggga([], T79, T80, .(T79, T80))
U2_ggga(T64, T65, T66, T67, T69, append1B_out_ggga(T65, T66, T67, T69)) → append1B_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U6_ga(T16, T17, T7, append1B_out_ggga(T21, T16, T20, T7)) → rotateD_out_ga(.(T16, T17), T7)
rotateD_in_ga(T86, T7) → U7_ga(T86, T7, append1C_in_ga(T86, T7))
append1C_in_ga(.(T102, T103), .(T102, T105)) → U3_ga(T102, T103, T105, append1C_in_ga(T103, T105))
append1C_in_ga([], []) → append1C_out_ga([], [])
U3_ga(T102, T103, T105, append1C_out_ga(T103, T105)) → append1C_out_ga(.(T102, T103), .(T102, T105))
U7_ga(T86, T7, append1C_out_ga(T86, T7)) → rotateD_out_ga(T86, T7)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
rotateD_in_ga(.(T16, T17), T7) → U4_ga(T16, T17, T7, append2A_in_aag(X40, X41, T17))
append2A_in_aag(.(T32, X89), X90, .(T32, T33)) → U1_aag(T32, X89, X90, T33, append2A_in_aag(X89, X90, T33))
append2A_in_aag([], T38, T38) → append2A_out_aag([], T38, T38)
U1_aag(T32, X89, X90, T33, append2A_out_aag(X89, X90, T33)) → append2A_out_aag(.(T32, X89), X90, .(T32, T33))
U4_ga(T16, T17, T7, append2A_out_aag(X40, X41, T17)) → rotateD_out_ga(.(T16, T17), T7)
rotateD_in_ga(.(T16, T17), T7) → U5_ga(T16, T17, T7, append2A_in_aag(T20, T21, T17))
U5_ga(T16, T17, T7, append2A_out_aag(T20, T21, T17)) → U6_ga(T16, T17, T7, append1B_in_ggga(T21, T16, T20, T7))
append1B_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U2_ggga(T64, T65, T66, T67, T69, append1B_in_ggga(T65, T66, T67, T69))
append1B_in_ggga([], T79, T80, .(T79, T80)) → append1B_out_ggga([], T79, T80, .(T79, T80))
U2_ggga(T64, T65, T66, T67, T69, append1B_out_ggga(T65, T66, T67, T69)) → append1B_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U6_ga(T16, T17, T7, append1B_out_ggga(T21, T16, T20, T7)) → rotateD_out_ga(.(T16, T17), T7)
rotateD_in_ga(T86, T7) → U7_ga(T86, T7, append1C_in_ga(T86, T7))
append1C_in_ga(.(T102, T103), .(T102, T105)) → U3_ga(T102, T103, T105, append1C_in_ga(T103, T105))
append1C_in_ga([], []) → append1C_out_ga([], [])
U3_ga(T102, T103, T105, append1C_out_ga(T103, T105)) → append1C_out_ga(.(T102, T103), .(T102, T105))
U7_ga(T86, T7, append1C_out_ga(T86, T7)) → rotateD_out_ga(T86, T7)
ROTATED_IN_GA(.(T16, T17), T7) → U4_GA(T16, T17, T7, append2A_in_aag(X40, X41, T17))
ROTATED_IN_GA(.(T16, T17), T7) → APPEND2A_IN_AAG(X40, X41, T17)
APPEND2A_IN_AAG(.(T32, X89), X90, .(T32, T33)) → U1_AAG(T32, X89, X90, T33, append2A_in_aag(X89, X90, T33))
APPEND2A_IN_AAG(.(T32, X89), X90, .(T32, T33)) → APPEND2A_IN_AAG(X89, X90, T33)
ROTATED_IN_GA(.(T16, T17), T7) → U5_GA(T16, T17, T7, append2A_in_aag(T20, T21, T17))
U5_GA(T16, T17, T7, append2A_out_aag(T20, T21, T17)) → U6_GA(T16, T17, T7, append1B_in_ggga(T21, T16, T20, T7))
U5_GA(T16, T17, T7, append2A_out_aag(T20, T21, T17)) → APPEND1B_IN_GGGA(T21, T16, T20, T7)
APPEND1B_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → U2_GGGA(T64, T65, T66, T67, T69, append1B_in_ggga(T65, T66, T67, T69))
APPEND1B_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → APPEND1B_IN_GGGA(T65, T66, T67, T69)
ROTATED_IN_GA(T86, T7) → U7_GA(T86, T7, append1C_in_ga(T86, T7))
ROTATED_IN_GA(T86, T7) → APPEND1C_IN_GA(T86, T7)
APPEND1C_IN_GA(.(T102, T103), .(T102, T105)) → U3_GA(T102, T103, T105, append1C_in_ga(T103, T105))
APPEND1C_IN_GA(.(T102, T103), .(T102, T105)) → APPEND1C_IN_GA(T103, T105)
rotateD_in_ga(.(T16, T17), T7) → U4_ga(T16, T17, T7, append2A_in_aag(X40, X41, T17))
append2A_in_aag(.(T32, X89), X90, .(T32, T33)) → U1_aag(T32, X89, X90, T33, append2A_in_aag(X89, X90, T33))
append2A_in_aag([], T38, T38) → append2A_out_aag([], T38, T38)
U1_aag(T32, X89, X90, T33, append2A_out_aag(X89, X90, T33)) → append2A_out_aag(.(T32, X89), X90, .(T32, T33))
U4_ga(T16, T17, T7, append2A_out_aag(X40, X41, T17)) → rotateD_out_ga(.(T16, T17), T7)
rotateD_in_ga(.(T16, T17), T7) → U5_ga(T16, T17, T7, append2A_in_aag(T20, T21, T17))
U5_ga(T16, T17, T7, append2A_out_aag(T20, T21, T17)) → U6_ga(T16, T17, T7, append1B_in_ggga(T21, T16, T20, T7))
append1B_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U2_ggga(T64, T65, T66, T67, T69, append1B_in_ggga(T65, T66, T67, T69))
append1B_in_ggga([], T79, T80, .(T79, T80)) → append1B_out_ggga([], T79, T80, .(T79, T80))
U2_ggga(T64, T65, T66, T67, T69, append1B_out_ggga(T65, T66, T67, T69)) → append1B_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U6_ga(T16, T17, T7, append1B_out_ggga(T21, T16, T20, T7)) → rotateD_out_ga(.(T16, T17), T7)
rotateD_in_ga(T86, T7) → U7_ga(T86, T7, append1C_in_ga(T86, T7))
append1C_in_ga(.(T102, T103), .(T102, T105)) → U3_ga(T102, T103, T105, append1C_in_ga(T103, T105))
append1C_in_ga([], []) → append1C_out_ga([], [])
U3_ga(T102, T103, T105, append1C_out_ga(T103, T105)) → append1C_out_ga(.(T102, T103), .(T102, T105))
U7_ga(T86, T7, append1C_out_ga(T86, T7)) → rotateD_out_ga(T86, T7)
ROTATED_IN_GA(.(T16, T17), T7) → U4_GA(T16, T17, T7, append2A_in_aag(X40, X41, T17))
ROTATED_IN_GA(.(T16, T17), T7) → APPEND2A_IN_AAG(X40, X41, T17)
APPEND2A_IN_AAG(.(T32, X89), X90, .(T32, T33)) → U1_AAG(T32, X89, X90, T33, append2A_in_aag(X89, X90, T33))
APPEND2A_IN_AAG(.(T32, X89), X90, .(T32, T33)) → APPEND2A_IN_AAG(X89, X90, T33)
ROTATED_IN_GA(.(T16, T17), T7) → U5_GA(T16, T17, T7, append2A_in_aag(T20, T21, T17))
U5_GA(T16, T17, T7, append2A_out_aag(T20, T21, T17)) → U6_GA(T16, T17, T7, append1B_in_ggga(T21, T16, T20, T7))
U5_GA(T16, T17, T7, append2A_out_aag(T20, T21, T17)) → APPEND1B_IN_GGGA(T21, T16, T20, T7)
APPEND1B_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → U2_GGGA(T64, T65, T66, T67, T69, append1B_in_ggga(T65, T66, T67, T69))
APPEND1B_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → APPEND1B_IN_GGGA(T65, T66, T67, T69)
ROTATED_IN_GA(T86, T7) → U7_GA(T86, T7, append1C_in_ga(T86, T7))
ROTATED_IN_GA(T86, T7) → APPEND1C_IN_GA(T86, T7)
APPEND1C_IN_GA(.(T102, T103), .(T102, T105)) → U3_GA(T102, T103, T105, append1C_in_ga(T103, T105))
APPEND1C_IN_GA(.(T102, T103), .(T102, T105)) → APPEND1C_IN_GA(T103, T105)
rotateD_in_ga(.(T16, T17), T7) → U4_ga(T16, T17, T7, append2A_in_aag(X40, X41, T17))
append2A_in_aag(.(T32, X89), X90, .(T32, T33)) → U1_aag(T32, X89, X90, T33, append2A_in_aag(X89, X90, T33))
append2A_in_aag([], T38, T38) → append2A_out_aag([], T38, T38)
U1_aag(T32, X89, X90, T33, append2A_out_aag(X89, X90, T33)) → append2A_out_aag(.(T32, X89), X90, .(T32, T33))
U4_ga(T16, T17, T7, append2A_out_aag(X40, X41, T17)) → rotateD_out_ga(.(T16, T17), T7)
rotateD_in_ga(.(T16, T17), T7) → U5_ga(T16, T17, T7, append2A_in_aag(T20, T21, T17))
U5_ga(T16, T17, T7, append2A_out_aag(T20, T21, T17)) → U6_ga(T16, T17, T7, append1B_in_ggga(T21, T16, T20, T7))
append1B_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U2_ggga(T64, T65, T66, T67, T69, append1B_in_ggga(T65, T66, T67, T69))
append1B_in_ggga([], T79, T80, .(T79, T80)) → append1B_out_ggga([], T79, T80, .(T79, T80))
U2_ggga(T64, T65, T66, T67, T69, append1B_out_ggga(T65, T66, T67, T69)) → append1B_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U6_ga(T16, T17, T7, append1B_out_ggga(T21, T16, T20, T7)) → rotateD_out_ga(.(T16, T17), T7)
rotateD_in_ga(T86, T7) → U7_ga(T86, T7, append1C_in_ga(T86, T7))
append1C_in_ga(.(T102, T103), .(T102, T105)) → U3_ga(T102, T103, T105, append1C_in_ga(T103, T105))
append1C_in_ga([], []) → append1C_out_ga([], [])
U3_ga(T102, T103, T105, append1C_out_ga(T103, T105)) → append1C_out_ga(.(T102, T103), .(T102, T105))
U7_ga(T86, T7, append1C_out_ga(T86, T7)) → rotateD_out_ga(T86, T7)
APPEND1C_IN_GA(.(T102, T103), .(T102, T105)) → APPEND1C_IN_GA(T103, T105)
rotateD_in_ga(.(T16, T17), T7) → U4_ga(T16, T17, T7, append2A_in_aag(X40, X41, T17))
append2A_in_aag(.(T32, X89), X90, .(T32, T33)) → U1_aag(T32, X89, X90, T33, append2A_in_aag(X89, X90, T33))
append2A_in_aag([], T38, T38) → append2A_out_aag([], T38, T38)
U1_aag(T32, X89, X90, T33, append2A_out_aag(X89, X90, T33)) → append2A_out_aag(.(T32, X89), X90, .(T32, T33))
U4_ga(T16, T17, T7, append2A_out_aag(X40, X41, T17)) → rotateD_out_ga(.(T16, T17), T7)
rotateD_in_ga(.(T16, T17), T7) → U5_ga(T16, T17, T7, append2A_in_aag(T20, T21, T17))
U5_ga(T16, T17, T7, append2A_out_aag(T20, T21, T17)) → U6_ga(T16, T17, T7, append1B_in_ggga(T21, T16, T20, T7))
append1B_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U2_ggga(T64, T65, T66, T67, T69, append1B_in_ggga(T65, T66, T67, T69))
append1B_in_ggga([], T79, T80, .(T79, T80)) → append1B_out_ggga([], T79, T80, .(T79, T80))
U2_ggga(T64, T65, T66, T67, T69, append1B_out_ggga(T65, T66, T67, T69)) → append1B_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U6_ga(T16, T17, T7, append1B_out_ggga(T21, T16, T20, T7)) → rotateD_out_ga(.(T16, T17), T7)
rotateD_in_ga(T86, T7) → U7_ga(T86, T7, append1C_in_ga(T86, T7))
append1C_in_ga(.(T102, T103), .(T102, T105)) → U3_ga(T102, T103, T105, append1C_in_ga(T103, T105))
append1C_in_ga([], []) → append1C_out_ga([], [])
U3_ga(T102, T103, T105, append1C_out_ga(T103, T105)) → append1C_out_ga(.(T102, T103), .(T102, T105))
U7_ga(T86, T7, append1C_out_ga(T86, T7)) → rotateD_out_ga(T86, T7)
APPEND1C_IN_GA(.(T102, T103), .(T102, T105)) → APPEND1C_IN_GA(T103, T105)
APPEND1C_IN_GA(.(T102, T103)) → APPEND1C_IN_GA(T103)
From the DPs we obtained the following set of size-change graphs:
APPEND1B_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → APPEND1B_IN_GGGA(T65, T66, T67, T69)
rotateD_in_ga(.(T16, T17), T7) → U4_ga(T16, T17, T7, append2A_in_aag(X40, X41, T17))
append2A_in_aag(.(T32, X89), X90, .(T32, T33)) → U1_aag(T32, X89, X90, T33, append2A_in_aag(X89, X90, T33))
append2A_in_aag([], T38, T38) → append2A_out_aag([], T38, T38)
U1_aag(T32, X89, X90, T33, append2A_out_aag(X89, X90, T33)) → append2A_out_aag(.(T32, X89), X90, .(T32, T33))
U4_ga(T16, T17, T7, append2A_out_aag(X40, X41, T17)) → rotateD_out_ga(.(T16, T17), T7)
rotateD_in_ga(.(T16, T17), T7) → U5_ga(T16, T17, T7, append2A_in_aag(T20, T21, T17))
U5_ga(T16, T17, T7, append2A_out_aag(T20, T21, T17)) → U6_ga(T16, T17, T7, append1B_in_ggga(T21, T16, T20, T7))
append1B_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U2_ggga(T64, T65, T66, T67, T69, append1B_in_ggga(T65, T66, T67, T69))
append1B_in_ggga([], T79, T80, .(T79, T80)) → append1B_out_ggga([], T79, T80, .(T79, T80))
U2_ggga(T64, T65, T66, T67, T69, append1B_out_ggga(T65, T66, T67, T69)) → append1B_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U6_ga(T16, T17, T7, append1B_out_ggga(T21, T16, T20, T7)) → rotateD_out_ga(.(T16, T17), T7)
rotateD_in_ga(T86, T7) → U7_ga(T86, T7, append1C_in_ga(T86, T7))
append1C_in_ga(.(T102, T103), .(T102, T105)) → U3_ga(T102, T103, T105, append1C_in_ga(T103, T105))
append1C_in_ga([], []) → append1C_out_ga([], [])
U3_ga(T102, T103, T105, append1C_out_ga(T103, T105)) → append1C_out_ga(.(T102, T103), .(T102, T105))
U7_ga(T86, T7, append1C_out_ga(T86, T7)) → rotateD_out_ga(T86, T7)
APPEND1B_IN_GGGA(.(T64, T65), T66, T67, .(T64, T69)) → APPEND1B_IN_GGGA(T65, T66, T67, T69)
APPEND1B_IN_GGGA(.(T64, T65), T66, T67) → APPEND1B_IN_GGGA(T65, T66, T67)
From the DPs we obtained the following set of size-change graphs:
APPEND2A_IN_AAG(.(T32, X89), X90, .(T32, T33)) → APPEND2A_IN_AAG(X89, X90, T33)
rotateD_in_ga(.(T16, T17), T7) → U4_ga(T16, T17, T7, append2A_in_aag(X40, X41, T17))
append2A_in_aag(.(T32, X89), X90, .(T32, T33)) → U1_aag(T32, X89, X90, T33, append2A_in_aag(X89, X90, T33))
append2A_in_aag([], T38, T38) → append2A_out_aag([], T38, T38)
U1_aag(T32, X89, X90, T33, append2A_out_aag(X89, X90, T33)) → append2A_out_aag(.(T32, X89), X90, .(T32, T33))
U4_ga(T16, T17, T7, append2A_out_aag(X40, X41, T17)) → rotateD_out_ga(.(T16, T17), T7)
rotateD_in_ga(.(T16, T17), T7) → U5_ga(T16, T17, T7, append2A_in_aag(T20, T21, T17))
U5_ga(T16, T17, T7, append2A_out_aag(T20, T21, T17)) → U6_ga(T16, T17, T7, append1B_in_ggga(T21, T16, T20, T7))
append1B_in_ggga(.(T64, T65), T66, T67, .(T64, T69)) → U2_ggga(T64, T65, T66, T67, T69, append1B_in_ggga(T65, T66, T67, T69))
append1B_in_ggga([], T79, T80, .(T79, T80)) → append1B_out_ggga([], T79, T80, .(T79, T80))
U2_ggga(T64, T65, T66, T67, T69, append1B_out_ggga(T65, T66, T67, T69)) → append1B_out_ggga(.(T64, T65), T66, T67, .(T64, T69))
U6_ga(T16, T17, T7, append1B_out_ggga(T21, T16, T20, T7)) → rotateD_out_ga(.(T16, T17), T7)
rotateD_in_ga(T86, T7) → U7_ga(T86, T7, append1C_in_ga(T86, T7))
append1C_in_ga(.(T102, T103), .(T102, T105)) → U3_ga(T102, T103, T105, append1C_in_ga(T103, T105))
append1C_in_ga([], []) → append1C_out_ga([], [])
U3_ga(T102, T103, T105, append1C_out_ga(T103, T105)) → append1C_out_ga(.(T102, T103), .(T102, T105))
U7_ga(T86, T7, append1C_out_ga(T86, T7)) → rotateD_out_ga(T86, T7)
APPEND2A_IN_AAG(.(T32, X89), X90, .(T32, T33)) → APPEND2A_IN_AAG(X89, X90, T33)
APPEND2A_IN_AAG(.(T32, T33)) → APPEND2A_IN_AAG(T33)
From the DPs we obtained the following set of size-change graphs: